R:es_realizer{i:l}, sv:(Id(T:Type{i}  (T + (T)))), av:(KndType{i}), dis:(IdId),
cl:(Id(n:  base-domain-type(n))es_realizer{i:l}), fr, rfr:(IdId(Knd List)),
sfr:(IdLnkId(Knd List)), afr:(IdKnd((Id List) + Top)), bfr:(IdKnd((IdLnk List) + Top)).
R-FeasibleWitness{i:l}(R; sv; av; dis; cl; fr; sfr; rfr; afr; bfr)  {i'} 

latex

Definitions

x,y,z,w,v. t(x;y;z;w;v), suptype(S; T), S  T, x,y. t(x;y), x,y,z,u,v,w. t(x;y;z;u;v;w), x,y,z. t(x;y;z), x. t(x), ff, tt, (i = j), p q, if b then t else f fi , x,y,z,w. t(x;y;z;w), P  Q, P & Q, R-FeasibleWitness, , t  T, Top, base-domain-type(n), x:A. B(x), x(s1,s2), x(s), x(s1,s2,s3,s4,s5), x(a,b,c,d,e,f), x(s1,s2,s3), x(s1,s2,s3,s4)

Lemmas

IdLnk wf, Id wf, Rrframe wf, Rbframe wf, Raframe wf, finite-prob-space wf, p-outcome wf, locl wf, Rpre wf, map wf, normal-ds wf, lnk-decl wf, Kind-deq wf, tagof wf, fpf-cap wf, eq lnk wf, Rsends wf, fpf wf, do-apply wf, top wf, can-apply wf, fpf-domain wf, l all wf2, l member wf, lnk wf, ldst wf, isrcv wf, fpf-trivial-subtype-top, fpf-dom wf, assert wf, id-deq wf, fpf-all wf, pi2 wf, decl-type wf, decl-state wf, Reffect wf, Rsframe wf, lsrc wf, Knd wf, pi1 wf, Rframe wf, isl wf, bool wf, rationals wf, Rinit wf, base-domain-type wf, Rnone wf, es realizer wf, es realizer ind wf